(declare-fun var0 () Int)
(declare-fun var3 () Bool)
(declare-fun var1 () Bool)
(declare-fun var4 () Bool)
(declare-fun var2 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () String)
(declare-fun var7 () String)
(declare-fun var8 () String)
(declare-fun var9 () String)
(declare-fun var10 () String)
(declare-fun var14 () Bool)
(declare-fun var11 () Bool)
(declare-fun var12 () Bool)
(declare-fun var13 () Bool)
(declare-fun var15 () String)
(assert (exists ((VAR0 Int)) (forall ((VAR0 Int)) (= (ite (= (mod 7 VAR0) 0) 1 0) 0))))
(assert (or (distinct var3 (= var1 var4)) (distinct var1 (distinct var2 0)) (distinct var3 (= var1 var4)) (ite (= var3 var4) (and (= var2 (+ var5 7)) (distinct var6 (str.++ var7 (str.substr var8 5 0))) (= var5 (str.len (str.substr var9 0 (str.len var10)))) (not (str.in_re (str.substr var9 4 (str.len var10)) (re.union (str.to_re "_") (str.to_re "u"))))) (str.in_re (str.substr var8 8 0) (str.to_re ""))) (= (ite (< (+ (mod 7 var0) var0) 7) 1 0) 0) var14 (= (ite (< (mod 7 var0) 7) 1 0) 0) (= (ite (< (+ (+ (mod 7 var0) var0) var0) 7) 1 0) 0)))
(assert (or (not (forall ((VAR12 Bool) (VAR11 Bool) (VAR3 Bool) (VAR3 Bool) (VAR0 Int) (VAR0 Int)) (xor (= (distinct VAR11 (= VAR12 var13)) (> 0 var2)) (= (ite (< (+ (mod 7 VAR0) VAR0) 7) 1 0) 0) (not var14)))) (not (forall ((VAR0 Int) (VAR2 Int) (VAR0 Int) (VAR11 Bool) (VAR13 Bool) (VAR2 Int)) (xor (= (distinct VAR11 (= var12 VAR13)) (> 0 VAR2)) (distinct var3 (= var1 var4)) (not var14))))))
(check-sat)
